◀ Prev · Parts · Full · Next ▶

JML specifications are added to Java code in the form of annotations in comments. Java comments are interpreted as JML annotations when they begin with an @ sign. That is, comments of the form

or

Basic JML syntax provides the following keywords

Defines a precondition on the method that follows.

Defines a postcondition on the method that follows.

Defines a postcondition for when a given Exception is thrown by the method that follows.

Defines what exceptions may be thrown when the given precondition holds.

Defines which fields are allowed to be assigned to by the method that follows.

Declares a method to be side effect free (like assignable \nothing but can also throw exceptions). Furthermore, a pure method is supposed to always either terminate normally or throw an exception.

Defines an invariant property of the class.

Defines a loop invariant for a loop.

Combines specification cases and can also declare that a method is inheriting specifications from its supertypes.

◀ Prev · Parts · Full · Next ▶